『Formal Specification: a Roadmap』

GPT-4.icon

概要:

形式的仕様は長年にわたりソフトウェアエンジニアリングの研究の焦点となっており、さまざまな設定で適用されてきました。

形式的仕様の本質、役割、使用法、落とし穴を再確認した後、これまでの主要な仕様パラダイムを検討し、その評価基準を議論します。

今日の形式的仕様技術の現在の強みと弱みを簡単に評価します。

今後のソフトウェアエンジニアリング活動の中核としての形式的仕様の要件を定式化します。

導入:

形式的仕様は、ある形式の言語で、ある抽象レベルで、システムが満たすべき一連のプロパティの表現です。

ソフトウェアアプリケーションは、開発ステップの一連の流れで構築されます。

形式的仕様は、文法的に整形された文のルール（構文）、文を特定のドメイン内で正確に意味のある方法で解釈するルール（セマンティクス）、および仕様から有用な情報を推論するルール（証明理論）で構成される言語で表現されます。

形式化: 範囲と落とし穴:

形式的仕様は、最初は形式的ではありません。

形式的仕様は、特定のドメインでの解釈方法を正確に定義することなくは意味を持たない。

形式的仕様の開発と評価は難しい。

仕様パラダイム:

形式的仕様技術は、特定の仕様パラダイムに依存する方法で主に異なります。

履歴ベースの仕様: システムを、時間を超えての許容される履歴（または「振る舞い」）の最大セットを特徴づけることで仕様としています。